Three independent commits, each droppable on its own. Two fix gates that could never fail; one fixes documentation that actively misdirects.

1. docs: — two files misstate the code they describe

PROOF-NEEDS.md

Claimed "1 Admitted in proofs/coq/lambda/LambdaCNO.v (y_not_cno)". Measured against absolute-zero @87902bb7:

$ grep -rn "Admitted" absolute-zero --include=*.v | wc -l
0
$ grep -rn "^Axiom"  absolute-zero --include=*.v | wc -l
23

Zero Admitted. Twenty-three Axioms across 6 files. The old wording was wrong in both directions — it overstated the incompleteness and understated the trusted base 23×.

Why this matters operationally: an Axiom passes a "no sorry / no Admitted" gate silently. Counting only Admitted measures the wrong thing.

y_not_cno is a KEPT AXIOM with a written rationale (LambdaCNO.v:388-399), not an unproven hole — and it is not the "concrete, closable proof obligation" the old text claimed. The in-source note explains it needs an invariant closed under the full reduction congruence, or a coinductive/step-indexed argument.

The doc now defers to the AXIOM AUDIT already in physics/LandauerDerivation.v, which is notably self-critical — it records that cno_zero_energy_dissipation_derived is an axiom despite its _derived name, and that the triage docs' "DISCHARGE" marks are inaccurate.

Promoted to the top of "What Needs Proving" — the audit's own SOUNDNESS WARNINGS: prob_nonneg and prob_normalized are false over unconstrained function-type distributions, and shannon_entropy_maximum's inequality is backwards (asserts uniform minimises entropy). All three are currently unused — cheap now, expensive later.

aletheia/CLAUDE.md

Said "all core logic lives in src/main.rs (~950 lines)" and "don't split into modules unless >1000 lines". It has been 5 modules / 995 lines for a while, main.rs at 121. That instruction would tell the next agent to undo the existing structure.

Also corrected: 23 workflows → 16; flake.nix listed but absent; 18 integration tests → 32. Added a prominent warning that those 16 nested workflows have never run (root-only discovery) — the fault that let this crate stay uncompilable for a month.

2. fix(aletheia): — the SHA-pinning check could never fail

if line.contains("@v") && !line.contains("@") {

contains("@v") implies contains("@"), so the second clause is always false and has_unpinned could never be set. Proven before changing anything:

uses: actions/checkout@v4    old_detects_unpinned=false

This is aletheia's Silver-level "GitHub Actions SHA pinning" check — and pointedly, the exact check that would have caught SonarSource/sonarqube-scan-action@master, the unpinned action that broke this repo's Governance and CodeQL in #139.

Replaced with uses_line_is_pinned, requiring 40 hex chars after the final @, which also:

• accepts the inline - uses: form (the estate's existing linter anchors to line-start and misses it)
• ignores a trailing # v7.0.1 provenance comment, so a correct pin with a stale comment isn't a false positive
• exempts ./… local actions/reusables and docker:// refs

Also replaced assert!(true) in test_file_exists with a real assertion, anchored on env!("CARGO_MANIFEST_DIR") so it is deterministic regardless of CWD.

Verified: 29 unit tests (was 26) · cargo fmt --check clean · clippy 25 → 23. End-to-end cargo run -- . now reports [FAIL] GitHub Actions SHA pinning, correctly finding the one genuinely unpinned action — where before the fix it reported a pass.

Refs #125.

3. fix(#99): — root Justfile was a fake gate

build:
    @echo "Build not configured yet"

build, test, fmt, lint, clean all printed a string and exited 0. Wired to the same commands root rust-ci.yml runs, in the same order, so just check means what CI means.

Two deliberate limits, documented in the recipes so nobody "fixes" them:

• test is --bins only — the integration suite is a spec for a CLI that doesn't exist; 27/29 fail by design (aletheia: 27/29 integration tests fail — main.rs never wires up the CLI surface #124). Adding --tests would make the bar green by breaking it.
• lint is not yet -D warnings (aletheia: clippy -D warnings has 25 findings — add as blocking gate once clean #125). When that closes it must be added here and to rust-ci.yml together, so local and CI never disagree.

Verified by running them, not reading them: just deps-check → OK: zero dependencies; just test → 29 passed; just check → exit 0.

And verified the gate can actually fail — appending badly-formatted Rust makes just fmt exit 1 while just build still exits 0; reverting restores 0. A gate nobody has watched fail is not a gate.

Closes #99.

Not in this PR

• aletheia: 27/29 integration tests fail — main.rs never wires up the CLI surface #124 — still blocked on the source-of-truth question for RSR checks
• guix.scm identity/licence clobber — separate, more urgent: fix: restore guix.scm identity and licence (squisher-corpus clobber is live on main) #143

🤖 Generated with Claude Code